﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace OpSatPlan.Encoder
{
    public class AtomicFormulaTemplate : VariableTemplate
    {
        private CnfEncoder mEncoder;
        private AtomicFormula mFormula;
        private int mOffset;
        private bool mValue;
		private int? mHashCode;
        public AtomicFormulaTemplate(CnfEncoder encoder, AtomicFormula formula, int offset, bool value)
        {
            this.mEncoder = encoder;
            this.mFormula = formula;
            this.mOffset = offset;
            this.mValue = value;
			this.mHashCode = null;
        }
        public override int GetVariable(int timeStep)
        {
            return (this.mValue ? 1 : -1) * this.mEncoder.GetVariable(this.mFormula, timeStep + this.mOffset);
        }
		public override int GetHashCode ()
		{
			if(this.mHashCode == null)
			{
				int result = 17;
                result = result * 37 + this.mFormula.GetHashCode();
				result = result * 37 + this.mValue.GetHashCode();
				result = result * 37 + this.mOffset.GetHashCode();
				this.mHashCode = result;
			}
			return this.mHashCode.Value;
		}
		public override bool Equals(object obj)
        {
            if (obj == null)
                return false;
            else if (obj.GetType() == typeof(AtomicFormulaTemplate))
                return this == (AtomicFormulaTemplate)obj;
            else
                return false;
        }

        public static bool operator ==(AtomicFormulaTemplate x, AtomicFormulaTemplate y)
        {
            if (System.Object.ReferenceEquals(x, y))
                return true;
            else if ((object)x == null || (object)y == null)
                return false;
            else
                return x.GetHashCode() == y.GetHashCode();

        }

        public static bool operator !=(AtomicFormulaTemplate x, AtomicFormulaTemplate y)
        {
            return !(x == y);
        }
    }
}
